Nuprl Lemma : remove-repeats_wf
0,22
postcript
pdf
T
:Type,
eq
:EqDecider(
T
),
L
:
T
List. remove-repeats(
eq
;
L
)
T
List
latex
Definitions
x
:
A
.
B
(
x
)
,
t
T
,
remove-repeats(
eq
;
L
)
Lemmas
l-union
wf
,
deq
wf
origin
T:Type, eq:EqDecider(T), L:T List. remove-repeats(eq;L) 
T List T:Type, eq:EqDecider(T), L:T List. remove-repeats(eq;L) T List x:A. B(x) T